(* ECORE *)
Require Import Int.
Require Import List.
Require Import String.
Require Import Datatypes.
Load Fin.

Inductive maybe X := nothing | just : X -> maybe X.
Global Implicit Arguments just [X].
Global Implicit Arguments nothing [X].


(** Definition Vec  (A:Set) (n:nat): Set := Fin n -> A.*)
Inductive Vec (A:Type) : nat -> Type :=
| Vnil : Vec A O
| Vcons : forall (n:nat), A-> Vec A n -> Vec A (S n).
Global Implicit Arguments Vnil  [A].
Global Implicit Arguments Vcons [A n].

Definition vec_in {A:Type}{n:nat}(comp: A -> A -> Prop): A -> Vec A n -> Prop.
intros.
induction X0.
apply False.
apply (comp X a /\ IHX0).
Defined.

Definition vec_notin {A:Type}{n:nat}(ncomp: A-> A-> Prop) : A-> Vec A n -> Prop.
intros.
induction X0.
apply True.
apply (ncomp X a /\ IHX0).
Defined.

Fixpoint vec_map {A B:Type}{n:nat}(f : A -> B)(v: Vec A n){struct v}: Vec B n
  := match v as v in Vec _ n return Vec _ n with
       | Vnil => Vnil (A:=B)
       | Vcons _ a aas => Vcons (f a) (vec_map f aas)
     end.


Section Emof2Set.

Variable TV : Set.

Section Element.
(** The named primitive types. Let's be conservative and not include
arbitrary other options **) 
(* names of classes *)
Variable PTR : Set. 





(** THE NOMINAL VERSION OF THE SPECIFICATION -- AS PER EMOF **)
(** HERE, PTR the set of names **)

Record MultiplicityElement := mkME{ 
(*  EME_isOrdered : bool; *) (* ordered attributes are lists, unordered attributes are ... ehm ... also lists, because the memory is finite *)
  EME_isUnique : bool; 
(* equality of classes is their pointer, and the appropriate notion
for the primitive types *)
  EME_lower : nat;
  EME_upper : maybe nat
} .

Record PropertySpec : Set := {
  propME : MultiplicityElement
(** the following attributes of properties have been ignored **)
(*  isRO : bool; *)
(* because we don't have a proper model of operations. Otherwise, we
   could translate a RO attribute to a getter and a R/W attribute to a
   getter/setter pair. But at this point, classes are just records and
   we are not considering operational behaviour at all. *)
(*  isComposite : bool; *) (* beyond our model *)
(*  isDerived : bool;*) (* has a very metaphysical meaning *)
(*  isID : bool *) (* ids of classes are their addresses *)
}.

Record Property : Set := {
  type : TV + PTR;  (* type can be either primitive or a proper class *) 
  one_end : PropertySpec;
  other_end : maybe (PropertySpec)
}.


(** replacing primitive types for arbitrary typed element on the covariant side of an operation **)
Record Operation : Set := {
  opME : MultiplicityElement;
  opType : TV + PTR; (* type can be either primitive or a proper class *)
  params : list (TV * MultiplicityElement) (* but no proper classes on the negative side *)

}.


Record ClassT : Set := {
  isAbstract : bool; 
  attributes : list Property;
  supers : list PTR; (* superclasses are always classes *)
  operations : list Operation
}.


(** Note that primitive types are unboxed **)
(** A system on a given set of names is a collection of classes. As
primitive types are unboxed and equality on primitive types is
equality of their values, not pointers to their boxes, it's safe to do
that. It would only start to be a problem if we considered the
operational behaviour of class diagrams, i.e. sharing of primitive
values. **) 

Definition EMOF_diagram : Set := PTR -> ClassT.
(* Of course, to get a complete interpretation of emof diagrams, we
will also need an assignment of Sets to TVs. There is no more one can
say about primitive types (then which sets they map to). That's why
they are called "primitive" after all. *)



(** a nondependent version of list induction **)
Definition foldr {A B:Set} (b:B) (g : A -> B -> B) : list A -> B :=
  list_rec (fun _ => B) b (fun a _ b => g a b).


(** some auxiliary functions on EMOF diagrams **)
(** retrieves the list of superclasses of a given class **)
Definition superclasses : EMOF_diagram -> PTR -> list (ClassT)
:= fun m p => map m (supers (m p)).


(** checks whether a given element is in the list **)
Fixpoint list_inb {A: Set} (eq : A -> A -> bool) (l:  list A) {struct l} :  A -> bool
:= fun a => match l with 
              | nil => false
              | cons x xs => orb (eq x a) (list_inb eq xs a)
            end.


(** simple boolean equality on natural numbers **)
Fixpoint nat_eqb ( m n : nat) {struct m} : bool 
:= 
match m with 
  | O => match n with 
           | O => true
           | _ => false
         end
  | S m' => match n with
              | O => false
              | S n' => nat_eqb m' n'
            end
end.

(** STRUCTURAL VERSION OF EMOF **)

(*constant types *)
(*Here we define a grammar of constant types built from the basic *)
(*constants -- type variables. Note that as we have no variable *)
(*binding, the only role of type variables is that of names for *)
(*constants. Here we allow the building of more elaborate constants *)
(*from the basic constants. Without this definition, it wouldn't be *)
(*legal to define a type such as (Nat->Nat) -> t , for some TT t below *)

(*It's essential that this is Inductive, not CoInductive *)
Inductive CT : Set :=
| KVar : TV -> CT
| KProd : CT -> CT -> CT
| KUnit : CT
| KCol : MultiplicityElement -> CT -> CT.



(*Strictly positive types *)
CoInductive SP : Set :=
(* Injection of constants *)
| SPConst  : CT -> SP
(* collections *)
| SPCol: MultiplicityElement -> SP -> SP 
(* Strictly positive function space *)
| SPFun : CT -> SP -> SP
(* Products *)
| SPProd : SP -> SP -> SP
(* Unit *)
| SPUnit : SP
(* Coproducts *)
| SPSum : SP -> SP -> SP 
(* Zero *)
| SPZero : SP.


End Element.

Implicit Arguments isAbstract [ PTR].
Implicit Arguments attributes [ PTR].
Implicit Arguments supers [ PTR].
Implicit Arguments operations [ PTR].
Implicit Arguments opME [ PTR].
Implicit Arguments opType [ PTR].
Implicit Arguments params [ PTR].
Implicit Arguments type [ PTR].
Implicit Arguments one_end [ PTR].
Implicit Arguments other_end [ PTR].
Implicit Arguments superclasses [ PTR].
Implicit Arguments Build_ClassT [ PTR].
Implicit Arguments Build_Property [ PTR].




(** we must start from a particular root class **)
Section THERE.
(** the translation between the nominal and structural version is.
   detailed below. Here is the core of what is supported and how,
   because from TT -> Set it's easy.  **)

(** Handling inheritance and subtyping: inheritance means that the
data for superclasses is part of the data for subclasses.  Subtyping
means that whereever a supertype can appear, any of its subtypes can
appear. Under the closed world assumption, this means that a supertype
is a sum of its subtypes.  Depending on whether a class is abstract or
not , C itself is included in the sum or not (this is not meant
recursively as subtyping and inheritance are separate concerns)

In short, all occurences of a class with superclasses in attributes
and or operations is replaced by a sum of its descendants.

Note that in order to be able to make this transition (from subtyping
to sums) we must assume enumerability of subclasses. Here we make our
life easy by assuming only a FINITE collection of classes, i.e. PTR is
Fin n for some n.
 **)


Variable n: nat.
Let Ptr := Fin n.
Variable m: EMOF_diagram Ptr.

(** Saying that every element uniqe in a list l is unique **)
Fixpoint isUnique {A:Set}(l:list A) {struct l}: Prop := 
  match l with 
    | nil => True
    | (x::xs) => (not (In x xs)) /\ isUnique xs
  end.


(** the meaining of collections **)
Definition buildCollection (me:MultiplicityElement) (A:Set) : Set
:= { l : list A | (List.length l >= (EME_lower me))
  /\ (match (EME_upper me) with just n => List.length l <= n | nothing => True end)
  /\ (if (EME_isUnique me) then (isUnique l) else True)
}.

Definition subclassPtrs : Ptr -> list Ptr
:= fun (i:Ptr) =>
  let l := @foldr Ptr (list Ptr)
    nil  
    (fun (x:Ptr) (l:list Ptr) => if (list_inb (fin_eqb (n:=n)) (supers (m x)) i) then (x :: l) else l)
    (enum_fin n)
    in if (isAbstract (m i)) then l else (i :: l).


(** turn pointers to subclasses into subclasses  -- just postcompose subclassPtrs with map m**)
Definition subclasses' : Fin n -> (list (ClassT (Fin n)))
:= fun i => map m (subclassPtrs i).


(** translation of parameters of operations into constant types *)
Fixpoint there_params (ps: list (TV * MultiplicityElement)) : CT
  := match ps with
       | nil => KUnit
       | cons p ps => KProd (KCol (snd p) (KVar (fst p))) (there_params ps)
     end.


(** The function infinitely unfolds the graph into a coinductive type **)
CoFixpoint there (i: Fin n): SP
  := let c := m i in SPProd (SPProd (there_attrs (attributes c) i)
  (there_prodclasses (supers c))) (there_operations (operations c))
with 
  there_attrs (attrs : list (Property (Fin n))) (rev:Fin n) :  SP 
  := match attrs with 
     | nil => SPUnit
     | cons a attrs' => SPProd (
(** turn a property into a collection of collections **)
       match (type a) with 
         | inl tv => SPConst (KVar tv)
(** here we do a U-Turn if necessary **)
(** Note that this is not a complete semantics as a model of A -- B is
   A*B but not (nu Y. A*(B*Y)) i.e. infinite iterating sequences of As
   and Bs. Currently, our model admits also the latter **)
         | inr ptr => SPCol (propME (one_end a)) (*(there_sumclasses (subclassPtrs ptr))*)
           (match  other_end a with
                                                    | nothing => there_sumclasses (subclassPtrs ptr)
                                                    | just e => SPProd 
                                                      (SPCol (propME e) (there_sumclasses (subclassPtrs rev)))
                                                      (there_sumclasses (subclassPtrs ptr))
                                                  end)
       end)
(** and the rest recursively **)
       (there_attrs attrs' rev)
     end
with
(** turning a list of classes into an iterative sum **)
  there_sumclasses (c: list (Fin n)) : SP
:= match c with
     | nil => SPZero
     | cons c cs => SPSum (there c) (there_sumclasses cs)
   end
(*       JoinT ((SumT (map there ()))::)::nil)*)
(*       (ColT (propME (one_end a))  (** collection in the target type **)*)
with
  there_prodclasses (cs : list (Fin n)) : SP
  :=  match cs with
        | nil => SPUnit
        | cons c cs => 
          SPProd (there c)(there_prodclasses cs)
      end
with
  there_operations (ops: list (Operation (Fin n))) : SP
  := match ops with 
       | nil => SPUnit
       | cons o ops =>
         SPProd (there_op o) (there_operations ops)
     end
with
  there_op (op:Operation (Fin n)) : SP 
  :=  SPFun (there_params (params op))
  (SPCol (opME op) (match opType op with
                      | inl tv => SPConst (KVar tv)
                      | inr c => there c
                    end)).
End THERE.

Section INTERPRETATION.
Variable n: nat.
Let Ptr := Fin n.
Variable m: EMOF_diagram Ptr.
Variable ENV : TV -> Set.

(** The inductive part of the mapping on constant types **)
Fixpoint CTImp (pt: CT) : Set :=
  match pt with
    | KUnit => unit
    | KVar tv => ENV tv
(*    | KFun d c => (CTImp d -> CTImp c)*)
    | KProd l r => ((CTImp l) * (CTImp r))%type
(*    | KSum l r => ((CTImp l) + (CTImp r))%type*)
(*    | KZero => Empty_set*)
    | KCol me t => buildCollection me (CTImp t)
  end.

Definition ctFst (l r : CT)  : (CTImp (KProd l r)) -> CTImp l.
intros.
simpl in H.
apply (fst H).
Defined.

Definition ctSnd (l r: CT) : (CTImp (KProd l r)) -> CTImp r.
intros.
apply (snd H).
Defined.

Definition ctPair (l r : CT) (A:Set): (A -> CTImp l) -> (A -> CTImp r) -> ( A -> CTImp (KProd l r)).
intros.
simpl.
split.
apply H. apply H1.
apply H0. apply H1.
Defined.

Lemma ctProj1 (l r : CT) ( A : Set) (f:A->CTImp l) (g:A->CTImp r): 
forall (a:A), (ctFst l r (ctPair l r A f g a)) = f a .
intros.
simpl.
reflexivity.
Qed.


Lemma ctProj2 (l r : CT) ( A : Set) (f:A->CTImp l) (g:A->CTImp r): 
forall (a:A), (ctSnd l r (ctPair l r A f g a)) = g a .
intros.
simpl.
reflexivity.
Qed.



(** Coinductive bit for SP **)
Variable me' : MultiplicityElement.

Section UNIQ_LIST.


Inductive LowUpList (A:Set): nat -> maybe nat -> Set
:=
| LowUpNil : forall (m : nat),  Vec A m -> LowUpList A m (just m)
| LowUpSuc : forall (m n : nat), LowUpList A m (just n) -> LowUpList A m (just (S n))
| LowUpInf : forall (m n : nat), LowUpList A m (just n) -> LowUpList A m nothing 
| LowUpCons : forall (m : nat) (n : nat), LowUpList A m (just n) -> A -> LowUpList A m (just (S n)).




(** LowUpUniqList A <> m (just n) P is the type of lists of length from m to n or \infty and such that 
   P x for any (x:A) holds iff x is fresh in the list **)
Inductive LowUpUniqList(A:Set)(neq:A->A->Prop) : nat -> maybe nat -> (A->Prop) -> Type
:=
| LowUpUniqNil : forall {m : nat}(v:  Vec A m), LowUpUniqList A neq m (just m) (fun (x:A) => vec_notin neq x v)
| LowUpUniqCons : forall {m : nat} {n : nat}{fresh:A->Prop}(a: A)(xs:LowUpUniqList A neq  m (just n) fresh),
  fresh a -> LowUpUniqList A neq  m (just (S n)) (fun (y:A) => fresh y /\ neq y a)
| LowUpUniqSuc : forall {m n : nat}{fresh:A->Prop}, LowUpUniqList A neq  m (just n) fresh -> LowUpUniqList A neq  m (just (S n)) fresh
| LowUpUniqInf : forall {m n : nat}{fresh:A->Prop}, LowUpUniqList A neq  m (just n) fresh -> LowUpUniqList A neq  m nothing fresh.


Fixpoint LUUlength {A:Set}{neq:A->A->Prop}{m : nat}{n: maybe nat}{P:A->Prop}(l:LowUpUniqList A neq m n P){struct l} :  nat
:= match l with
     | LowUpUniqNil _ _ => m
     | LowUpUniqCons m n fresh x xs p => S (LUUlength xs)
     | LowUpUniqSuc m n f xs => LUUlength xs
     | LowUpUniqInf m n f xs => LUUlength xs
   end.

Fixpoint LUmap {A B : Set}{m:nat}{n:maybe nat} (f:A->B) (x: LowUpList A m n) {struct x}: LowUpList B m n
:= match x as x in LowUpList _ m n return LowUpList B m n
                with
                | LowUpNil m v => LowUpNil B m (vec_map f v)
                | LowUpSuc m n l => LowUpSuc B m n (LUmap f l)
                | LowUpInf m n l => LowUpInf B m n (LUmap f l)
                | LowUpCons m n l a => LowUpCons B m n (LUmap f l) (f a)
              end.

End  UNIQ_LIST.
Definition noteq := (fun x y => not (EqNat.eq_nat x y)).

Implicit Arguments LowUpUniqNil [ m].
Implicit Arguments LowUpUniqCons [ m n fresh].
Implicit Arguments LowUpUniqSuc [m n fresh].
Implicit Arguments LowUpUniqInf [m n fresh].

(* Definition list_from_2_to_3 : LowUpUniqList nat ntoeq 2 3   *)
(* ... here I need a property that any x is fresh in the rest of the list ... *)
(* LowUpUniqCons nat noteq 1 (LowUpUniqNil nat noteq (Vcons 3 (Vcons 3 (Vnil))))  *)
(* Eval compute in (LUUlength list_from_2_to_3). *)

(* Lemma LUUlist_min_length {m : nat}{n:maybe nat}{fresh ( *)




CoInductive ClassGraph : SP -> Set :=
| CGConst : forall (pt:CT), CTImp (pt) -> ClassGraph (SPConst pt)
(** buildCollection missing -- inline ? should work **)
(** We'd like to write something like:
| CGCol : forall (me:MultiplicityElement) (tt:SP), 
buildCollection me (ClassGraph tt) -> ClassGraph (SPCol me tt)

But the type built by buildCollection involves predicates on
(ClassGraph tt) and is therefore not strictly positive.

It's easy enough to get around the size issues using the definition of
low-up list above. We simply define a list of size i, n <= i <= m+\infty
as a vector of size n followed by a list of size at most (m-n) +
\infty. Here, we have merged these into the above definition of
LowUpList, which is just a vector of size at most m+\infty where nil
is constructed already from a vector of size n.

To encode uniqueness, we could try to use Connor's / Capretas
impredicative encoding of uniqe lists in LowUpUniqueList, where we
switch uniqueness off simply by feeding it with a comparison function
that says always False. The problem now is, however, how to compare
classes for uniqueness. 
*)
| CGCol : forall (me:MultiplicityElement) (tt:SP),
(*   { l : list (Fin m) | (List.length l >= (EME_lower me)) *)
(*     /\ (match (EME_upper me) with inl n => List.length l <= n | inr _ => True end) *)
(*     /\ (if (EME_isUnique me) then (isUnique l) else True) (** WRONG: Just checks uniqueness of indices **) *)
(*   } -> (Fin m -> ClassGraph (tt)) ->  *)
  LowUpList (ClassGraph tt) (EME_lower me) (EME_upper me) -> ClassGraph (SPCol me tt)
(* not strictly positive : because I cannot apply a strictly positive type to any term. *)
| CGFun : forall (t: CT) (t':SP), (CTImp t -> ClassGraph t') -> ClassGraph (SPFun t t') 
| CGProd : forall (t t': SP), ClassGraph t -> ClassGraph t' -> ClassGraph (SPProd t t') 
| CGUnit : ClassGraph (SPUnit)
| CGSumLeft : forall (t t': SP), ClassGraph t -> ClassGraph (SPSum t t')
| CGSumRight : forall (t t': SP), ClassGraph t' -> ClassGraph (SPSum t t').
(* | CGZero  -- no way *)



(*
| SPConst  : CT -> SP
| SPCol: MultiplicityElement -> SP -> SP 
| SPFun : CT -> SP -> SP
| SPProd : SP -> SP -> SP
| SPUnit : SP
| SPSum : SP -> SP -> SP 
| SPZero : SP.
*)





End INTERPRETATION.

End Emof2Set.
Global Implicit Arguments CGProd [ENV TV].
Global Implicit Arguments CGSumLeft [ENV TV].
Global Implicit Arguments CGSumRight [ENV TV].
Global Implicit Arguments CGUnit [ENV TV].      
Global Implicit Arguments CGCol [ENV TV].
Global Implicit Arguments CGFun [ENV TV].
Global Implicit Arguments CGConst [ENV TV].

Global Implicit Arguments SPProd [ TV].
Global Implicit Arguments SPSum [ TV].
Global Implicit Arguments SPUnit [ TV].      
Global Implicit Arguments SPZero [ TV].
Global Implicit Arguments SPCol [ TV].
Global Implicit Arguments SPFun [ TV].
Global Implicit Arguments SPConst [ TV].

Global Implicit Arguments KVar [TV].
Global Implicit Arguments KProd [TV].
Global Implicit Arguments KCol [TV].
Global Implicit Arguments KUnit [TV].

Global Implicit Arguments isAbstract [TV PTR].
Global Implicit Arguments attributes [TV PTR].
Global Implicit Arguments supers [TV PTR].
Global Implicit Arguments operations [TV PTR].
Global Implicit Arguments opME [TV PTR].
Global Implicit Arguments opType [TV PTR].
Global Implicit Arguments params [TV PTR].
Global Implicit Arguments type [TV PTR].
Global Implicit Arguments one_end [TV PTR].
Global Implicit Arguments other_end [TV PTR].
Global Implicit Arguments superclasses [TV PTR].
Global Implicit Arguments Build_ClassT [TV PTR].
Global Implicit Arguments Build_Property [TV PTR].



Section Example.

Inductive TV : Set := Str | Nat | Bool .


Let PTR := Fin 4.
Let Named := finNil 3.
Let Table := finSuc (finNil 2).
Let Column := finSuc (finSuc (finNil 1)).
Let TType := finSuc (finSuc (finSuc (finNil 0))).

Example named : ClassT TV PTR 
  := Build_ClassT 
  true  (* isAbstract *)
  ((Build_Property (inl PTR Str) (Build_PropertySpec (mkME true 1 (just 1))) nothing)
    ::nil) (* props *)
  nil  (* supers *)
  nil. (* operations *)



Example table : ClassT TV PTR 
  := Build_ClassT false 
  ((Build_Property 
    (inr TV Column) 
    (Build_PropertySpec (mkME true 0 nothing)) 
    (*just (Build_PropertySpec (mkME false 1 (just 1)))*) nothing
    ::
    (
      Build_Property (inr TV Column) 
      (Build_PropertySpec (mkME true 1 (just 1))) (* key *)
      (*just (Build_PropertySpec (mkME false 1 nothing))*) (* keyOf *) nothing
    )::nil))  (* properties *)
  (Named :: nil)
  nil.
    

Example column : ClassT TV PTR 
  := Build_ClassT false
  (Build_Property 
    (inr TV TType)
    (Build_PropertySpec (mkME false 1 (just 1)))
    (*just (Build_PropertySpec (mkME false 0 nothing))*) nothing
    :: nil ) (* properties *)
  (Named :: nil) (* superclasses *)
  nil.

Example ttype : ClassT TV PTR
  := Build_ClassT false
  nil (Named :: nil) nil.
    
Example ex_emof_diagram : EMOF_diagram TV PTR.
intros p.
inversion p.
exact named.
inversion H0.
exact table.
inversion H2.
exact column.
inversion H4.
exact ttype.
inversion H6.
Defined.

Lemma l1: ex_emof_diagram Named = named.
reflexivity. Qed.

Lemma l2: ex_emof_diagram Table = table.
reflexivity. Qed.

Lemma l3: ex_emof_diagram Column = column.
reflexivity. Qed.
 
Lemma l4: ex_emof_diagram TType = ttype.
reflexivity. Qed.

Check (there TV 4 ex_emof_diagram Named).


(* the long version *)
Eval compute in (there TV 4 ex_emof_diagram Named).

Definition eval1 (e: SP TV) (f:SP TV -> SP TV): SP TV
:=  match e with
      | SPConst  c => SPConst  c
      | SPCol me sp => SPCol  me (f sp)
      | SPFun ct sp => SPFun  ct (f sp)
      | SPProd x y => SPProd  (f x) (f y)
      | SPUnit  => SPUnit 
      | SPSum x y => SPSum  (f x) (f y)
      | SPZero => SPZero 
    end.

Fixpoint evaln (n:nat) (e:SP TV) { struct n} : SP TV
:= match n with
     | 0 => e
     | S n' => eval1 e (evaln n')
   end.

Lemma eval1_id : forall (e:SP TV) (f:SP TV -> SP TV) (H: forall x:SP TV, f x = x), eval1 e f = e.
intros.
case e.
reflexivity.
intros.
simpl.
rewrite H.
reflexivity.
simpl.
intros.
rewrite H.
reflexivity.
intros.
simpl.
repeat rewrite H.
reflexivity.
simpl.
reflexivity.
intros.
simpl.
repeat rewrite H.
reflexivity.
simpl.
reflexivity.
Qed.

Theorem evaln_id : forall (n:nat) (e:SP TV) , evaln n e = e.
fix 1.
intros.
case n.
simpl.
reflexivity.
simpl.
intros.
rewrite (eval1_id).
reflexivity.
intros.
rewrite evaln_id.
reflexivity.
Qed.

Let SP_named : SP TV := there TV 4 ex_emof_diagram Named.
Let SP_table : SP TV := there TV 4 ex_emof_diagram Table.
Let SP_column : SP TV := there TV 4 ex_emof_diagram Column.
Let SP_ttype : SP TV := there TV 4 ex_emof_diagram TType.
Eval compute in (evaln 100 SP_named).
Eval compute in (evaln 100 SP_table).
Eval compute in (evaln 100 SP_column).
Eval compute in (evaln 100 SP_ttype).

Lemma SP_ttype_eval : SP_ttype =  
      SPProd
         (SPProd SPUnit
            (SPProd
               (SPProd (SPProd (SPProd (SPConst (KVar Str)) SPUnit) SPUnit)
                  SPUnit) SPUnit)) SPUnit.
unfold SP_ttype.
rewrite <- (evaln_id 100 (there TV 4 ex_emof_diagram TType)).
simpl.
reflexivity.
Qed.


Definition ENV : TV -> Set 
:= fun v => match v with
              | Str => string
              | Nat => nat
              | Bool => bool
            end.

Eval compute in (ClassGraph TV ENV (evaln 100 SP_ttype)).

(*
Definition CG_eval1 {s : SP TV} : ClassGraph TV ENV s -> ClassGraph TV ENV s
:= fun x => match x with
              | CGProd a b x y => CGProd a b x y
              | CGUnit => CGUnit
              | CGSumLeft a b x => CGSumLeft a b x
              | CGSumRight a b x => CGSumRight a b x
              | CGConst c i => CGConst c i
              | CGFun t u f => CGFun t u f
              | CGCol m t l => CGCol m t l
            end.

Lemma CG_eval1_id { s : SP TV } : forall (x: ClassGraph TV ENV s) , CG_eval1 x = x .
intros s x.
case x.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
reflexivity.
Qed.

Fixpoint CG_evaln { s : SP TV} (n: nat) {struct n} :  ClassGraph TV ENV s -> ClassGraph TV ENV s
:= fun x => match n with
              | 0 => x
              | S n' => CG_eval1 (CG_evaln n' x)
            end.

Lemma CG_evaln_id {s : SP TV} : forall (n:nat)(x:ClassGraph TV ENV s), CG_evaln n x = x.
intros s.
induction n.
reflexivity.
intros x.
unfold CG_evaln.
rewrite CG_eval1_id.
apply IHn.
Qed.
*)
Eval compute in (ClassGraph TV ENV (evaln 100 SP_ttype)).
(*Eval compute in (CG_evaln 100 (ClassGraph TV ENV (evaln 100 SP_ttype))).*)


Definition CG_named : Set := ClassGraph TV ENV SP_named.
Eval compute in  CG_named.
Eval compute in (ClassGraph TV ENV (evaln 100 SP_named)).
Definition simpled_sp_named := SPProd (SPProd (SPProd (SPConst (KVar Str)) SPUnit) SPUnit) SPUnit.
Definition simpled_cg_named := ClassGraph TV ENV simpled_sp_named.

Lemma full_is_simpled: CG_named = simpled_cg_named.
unfold CG_named.
rewrite <- (evaln_id 100 SP_named).
reflexivity.
Defined.



Definition CG_table := ClassGraph TV ENV SP_table.
Definition CG_ttype := ClassGraph TV ENV SP_ttype.


Definition ttype_string : CG_ttype.
unfold CG_ttype;rewrite <- (evaln_id 100 SP_ttype);simpl.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
simpl.
apply ("string"%string).
constructor.
constructor.
constructor. 
constructor.
constructor.
Defined.

Definition ttype_string' : ClassGraph TV ENV (evaln 100 SP_ttype).
simpl.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
simpl.
apply ("string"%string).
constructor.
constructor.
constructor. 
constructor.
constructor.
Defined.

Check (CGProd _ _
     (CGProd _ _
       CGUnit
        (CGProd _ _
           (CGProd _ _
              (CGProd _ _ 
                 (CGProd _ _ 
                    (CGConst (KVar Str) "string"%string) CGUnit) 
                 CGUnit)
              CGUnit) 
           CGUnit)) 
     CGUnit (ENV:=ENV)).

Eval compute in evaln 100 SP_ttype.


Definition ttype_nat  : CG_ttype.
unfold CG_ttype;rewrite <- (evaln_id 100 SP_ttype);simpl.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
simpl.
apply ("nat"%string).
constructor.
constructor.
constructor. 
constructor.
constructor.
Defined.

Definition ttype_nat' : ClassGraph TV ENV (evaln 100 SP_ttype).
simpl.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
simpl.
apply ("nat"%string).
constructor.
constructor.
constructor. 
constructor.
constructor.
Defined.


Definition CG_column : Set :=  ClassGraph TV ENV SP_column.

Definition simplify {s : SP TV}(n:nat): ClassGraph TV ENV s -> ClassGraph TV ENV (evaln n s). 
intros.
rewrite evaln_id.
exact H.
Defined.


Definition column_name : CG_column.
unfold CG_column;rewrite <- (evaln_id 100 SP_column);simpl.
constructor.
constructor.
constructor.
constructor.
constructor.
apply Vcons.
apply CGSumLeft.
exact (simplify 100 ttype_string).
apply Vnil.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
apply ("name"%string).
constructor.
constructor.
constructor.
constructor.
constructor.
Defined.

Definition column_name' : ClassGraph TV ENV (evaln 100 SP_column).
simpl.
constructor.
constructor.
constructor.
constructor.
constructor.
apply Vcons.
apply CGSumLeft.
exact ttype_string'.
apply Vnil.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
apply ("name"%string).
constructor.
constructor.
constructor.
constructor.
constructor.
Defined.


Definition Iso ( A B : Type )  := { f:A->B & { g:B->A | (forall (a:A) , g (f a) = a) /\ (forall (b:B), f (g b) = b)}}.

Definition Prod_pi1 (a b : SP TV): ClassGraph TV ENV (SPProd a b) -> ClassGraph TV ENV a.  
intros a b.
intros.
inversion H.
exact H2.
Defined.

Definition Prod_pi2 (a b : SP TV): ClassGraph TV ENV (SPProd a b) -> ClassGraph TV ENV b.  
intros.
inversion H.
exact H3.
Defined.

Lemma Prod_pi1_id : forall ( a b : SP TV) (h1:ClassGraph TV ENV a) (h2 : ClassGraph TV ENV b) , Prod_pi1 a b (CGProd a b h1 h2) = h1. 
reflexivity.
Qed.

Definition Prod_inj1 (a : SP TV): ClassGraph TV ENV a -> ClassGraph TV ENV (SPProd a (SPUnit)).
intros.
constructor.
exact H.
constructor.
Defined.

(* Lemma CGProd_inversion : forall (a b : SP TV) (c: ClassGraph TV ENV (SPProd TV a b)), { j : ClassGraph TV ENV a & { k : ClassGraph TV ENV b | c = CGProd TV ENV  a b j k }}. *)
(* intros a b c. *)
(* inversion c. *)
(* exists H1. *)
(* exists H2. *)
(* simpl. *)
(* reflexivity. *)
(* inversion c. *)
(* exists H1. *)
(* exists H2. *)
(* case a. *)
(* case c. *)
(* reflexivity. *)

Definition eval1_CG ( a b: SP TV) 
  (f:ClassGraph TV ENV a -> ClassGraph TV ENV a) 
  (g:ClassGraph TV ENV b -> ClassGraph TV ENV b): 
  ClassGraph TV ENV (SPProd a b) -> ClassGraph TV ENV (SPProd a b).
intros.
inversion H.
apply CGProd.
exact H2.
exact H3.
Defined.

Inductive X : nat -> Set := XZero : X 0.

Definition Xinv : forall (x:X 0), x = XZero :=
fun x : X 0 =>
match x 
  as x0 in (X n)
  return
    (match n return (X n -> Prop) with
       | 0 => fun x1 : X 0 => x1 = XZero
       | S n => fun _ : X (S n) => True
     end x0)
with
  | XZero => refl_equal XZero
end.
Check (X_rect).



Definition Xinv' : forall (x:X 0), x = XZero :=
  X_rect (fun n => match n return (X n -> Prop) with 
                       | 0 => fun x1 : X 0 => x1 = XZero
                       | S n => fun _ : X (S n) => True
                     end) (refl_equal XZero) 0.


Definition xxx (a b : nat) : { a : nat & { b : nat | True}}.
intros.
exists a.
exists b.
trivial.
Defined.

Definition CGUnit_Inv : forall (h: ClassGraph TV ENV SPUnit), h = CGUnit
:=
fun h => match h as h in ClassGraph _ _ s return 
              (match s return (ClassGraph TV ENV s -> Prop) with
                 | SPProd a b => fun _ => True 
                 | SPConst _ => fun _ => True
                 | SPCol _ _ => fun _ => True
                 | SPFun _ _ => fun _ => True
                 | SPUnit => fun u => u = CGUnit
                 | SPSum _ _ => fun _ => True
                 | SPZero => fun _ => True
               end h) with
                  | CGProd _ _ x y => I
                  | CGConst _ _ => I
                  | CGCol _ _ _  => I
                  | CGFun _ _ _ => I
                  | CGUnit => refl_equal _
                  | CGSumLeft _ _ _ => I
                  | CGSumRight _ _  _ => I
                end.



Definition CGProd_Inv {a b : SP TV}
  : forall (h:ClassGraph TV ENV (SPProd a b)), { xy : ClassGraph TV ENV a * ClassGraph TV ENV b | h = CGProd a b (fst xy) (snd xy)}
    := fun h => match h as h in ClassGraph _ _ s return 
              (match s return (ClassGraph TV ENV s -> Set) with
                 | SPProd a b => 
                   fun h => { xy : ClassGraph TV ENV a * ClassGraph TV ENV b | h = CGProd a b (fst xy) (snd xy)}
                 | SPConst _ => fun _ => unit
                 | SPCol _ _ => fun _ => unit
                 | SPFun _ _ => fun _ => unit
                 | SPUnit => fun _ => unit
                 | SPSum _ _ => fun _ => unit
                 | SPZero => fun _ => unit
               end h) with
                  | CGProd _ _ x y => exist _ (x,y) (refl_equal _)
                  | CGConst _ _ => tt
                  | CGCol _ _ _  => tt
                  | CGFun _ _ _ => tt
                  | CGUnit => tt
                  | CGSumLeft _ _ _ => tt
                  | CGSumRight _ _ _ => tt
                end.

                    
Definition CGProd_fst {a b : SP TV} (h: ClassGraph TV ENV (SPProd a b)) : ClassGraph TV ENV a
:= match CGProd_Inv h  with
     | exist xy _ => fst xy
   end.

Definition CGProd_snd {a b : SP TV} (h: ClassGraph TV ENV (SPProd a b)) : ClassGraph TV ENV b
:= match CGProd_Inv h  with
     | exist xy _ => snd xy
   end.

Definition CGProd_from_product { a b : SP TV } : ClassGraph TV ENV a * ClassGraph TV ENV b -> ClassGraph TV ENV (SPProd a b)
:= fun x => CGProd a b (fst x) (snd x).

Definition CGProd_to_product { a b : SP TV}: ClassGraph TV ENV (SPProd a b) -> (ClassGraph TV ENV a * ClassGraph TV ENV b).
intros.
apply (let (xy,_) := (CGProd_Inv H ) in xy).
Defined.

Lemma CGProd_to_from_product_id { a b : SP TV} : forall (x:ClassGraph TV ENV a * ClassGraph TV ENV b) , CGProd_to_product (CGProd_from_product x) = x.
intros.
case x.
reflexivity.
Qed.


Lemma CGProd_from_to_product_id { a b : SP TV} : forall (x : ClassGraph TV ENV (SPProd a b)), CGProd_from_product (CGProd_to_product x) = x.
intros.
unfold CGProd_to_product.
unfold CGProd_from_product.
elim (CGProd_Inv x).
intros x0 H.
symmetry.
exact H.
Qed.

(** we have established an isomorphism: ClassGraph TV ENV (SPProd a b) is (ClassGraph TV ENV a * ClassGraph TV ENV b) **)

(** and we can use it to establish the following osomorphism **)
Definition CGProd_from_times_unit {a : SP TV} :  ClassGraph TV ENV (SPProd a (SPUnit)) ->(ClassGraph TV ENV a)
:= fun x => fst (CGProd_to_product x).

Lemma CGProd_Iso1 ( a : SP TV) :  Iso (ClassGraph TV ENV (SPProd a (SPUnit))) (ClassGraph TV ENV a).
intros.
unfold Iso.
exists (CGProd_from_times_unit).
exists (fun x => CGProd_from_product (x,CGUnit)).
split.
intros.
cutrewrite (CGUnit = snd (CGProd_to_product a0)).
Lemma fst_snd_id (A B : Type): forall x : A*B, (fst x, snd x) = x.
intros.
case x.
reflexivity.
Qed.
unfold CGProd_from_times_unit.
rewrite fst_snd_id.
apply CGProd_from_to_product_id.
elim (CGProd_to_product a0).
simpl.
intros.
rewrite CGUnit_Inv.
reflexivity.
intros.
unfold CGProd_from_times_unit.
rewrite CGProd_to_from_product_id.
reflexivity.
Qed.

(** so the isomorphism for products is done. Sums etc are similar. The
   following is going further: lifting reductions on SPs to reductions on CGs **)

Definition CGSum_Inv {a b : SP TV}
  : forall (h:ClassGraph TV ENV (SPSum a b)), 
    { x_or_y : ClassGraph TV ENV a + ClassGraph TV ENV b | 
      match x_or_y with
        | inl t => h = CGSumLeft a b t 
        | inr t' => h = CGSumRight a b t' 
      end }
    := fun h => match h as h in ClassGraph _ _ s return 
              (match s return (ClassGraph TV ENV s -> Set) with
                 | SPProd _ _ => fun _ => unit
                 | SPConst _ => fun _ => unit
                 | SPCol _ _ => fun _ => unit
                 | SPFun _ _ => fun _ => unit
                 | SPUnit => fun _ => unit
                 | SPSum a' b' => fun h' => 
                   { x_or_y : ClassGraph TV ENV a' + ClassGraph TV ENV b' | 
                     match x_or_y  with 
                            | inl t => h' = CGSumLeft a' b' t 
                            | inr t' => h' = CGSumRight a' b' t' 
                          end }
                 | SPZero => fun _ => unit
               end h) with
                  | CGProd _ _ _ _ => tt
                  | CGConst _ _ => tt
                  | CGCol _ _ _  => tt
                  | CGFun _ _ _ => tt
                  | CGUnit => tt
                  | CGSumLeft a b t => exist _ (inl (ClassGraph TV ENV b) t) (refl_equal _)
                  | CGSumRight a b t' => exist _ (inr (ClassGraph TV ENV a) t') (refl_equal _)
                end.


Definition CGSum_to_sum { a b : SP TV } : ClassGraph TV ENV (SPSum a b) -> ClassGraph TV ENV a + ClassGraph TV ENV b
:= fun h => let (x,_) := CGSum_Inv h in x. 

Definition CGSum_from_sum { a b : SP TV} : ClassGraph TV ENV a + ClassGraph TV ENV b ->  ClassGraph TV ENV (SPSum a b)
:= fun h => match h with
              | inl t => CGSumLeft _ _ t
              | inr t' => CGSumRight _ _ t'
            end.

Lemma CGSum_to_from_sum_id {a b : SP TV} : forall h:ClassGraph TV ENV a + ClassGraph TV ENV b, CGSum_to_sum (CGSum_from_sum h) = h.
intros.
case h.
reflexivity.
reflexivity.
Qed.

Lemma CGSum_from_to_sum_id {a b : SP TV} : forall h : ClassGraph TV ENV (SPSum a b), CGSum_from_sum (CGSum_to_sum h) = h.
intros.
unfold CGSum_from_sum.
unfold CGSum_to_sum.
simpl.
elim (CGSum_Inv h).
intros x.
elim x.
intros.
symmetry.
exact p.
intros ; symmetry.
exact p.
Qed.

Definition CGZero_Inv : ClassGraph TV ENV SPZero -> Empty_set
:= 
fun (h:ClassGraph TV ENV SPZero) 
  => match h as h in ClassGraph _ _ s return 
       (match s return (ClassGraph TV ENV s -> Set) with
          | SPProd a b => fun _ => unit 
          | SPConst _ => fun _ => unit
          | SPCol _ _ => fun _ => unit
          | SPFun _ _ => fun _ => unit
          | SPUnit => fun u => unit
          | SPSum _ _ => fun _ => unit
          | SPZero => fun _ => Empty_set
        end h) 
       with
       | CGProd _ _ _ _ => tt
       | CGConst _ _ => tt
       | CGCol _ _ _  => tt
       | CGFun _ _ _ => tt
       | CGUnit => tt
       | CGSumLeft _ _ _ => tt
       | CGSumRight _ _  _ => tt
     end.


Definition CGSum_from_pluszero { a: SP TV} : ClassGraph TV ENV (SPSum a SPZero) -> ClassGraph TV ENV a
:= fun h => 
  match CGSum_to_sum h with
    | inl x => x
    | inr y => match (CGZero_Inv y) with end
  end.

Definition CGSum_to_pluszero { a : SP TV } : ClassGraph TV ENV a -> ClassGraph TV ENV (SPSum a SPZero)
:= fun h => CGSum_from_sum (inl (ClassGraph TV ENV SPZero) h).

Definition CGSum_zero_iso { a : SP TV} : Iso (ClassGraph TV ENV (SPSum a SPZero)) (ClassGraph TV ENV  a).
intros.
exists CGSum_from_pluszero.
exists CGSum_to_pluszero.
split.
intros.
unfold CGSum_to_pluszero.
unfold CGSum_from_pluszero.
unfold CGSum_from_sum.
unfold CGSum_to_sum.
elim (CGSum_Inv a0).
intros x.
case x.
auto.
intros.
elim (CGZero_Inv c).
auto.
Defined.





Definition SP_reduceR1 (s:SP TV) : SP TV
:= match s with
     | SPProd x SPUnit => x
     | SPProd x (SPConst c) => SPProd x (SPConst c)
     | SPProd x (SPCol m t) => SPProd x (SPCol m t)
     | SPProd x (SPFun a b) => SPProd x (SPFun a b)
     | SPProd x (SPProd y z) =>  SPProd x (SPProd y z) 
     | SPProd x (SPSum a b ) => SPProd x (SPSum a b ) 
     | SPProd x SPZero => SPProd x SPZero
     | SPZero => SPZero
     | SPUnit => SPUnit
     | SPConst c => SPConst c
     | SPCol a b => SPCol a b
     | SPFun a b => SPFun a b 
     | SPSum a SPZero => a
     | SPSum a (SPConst c) => SPSum a (SPConst c)
     | SPSum a (SPCol b c) => SPSum a (SPCol b c)
     | SPSum a (SPFun b c) => SPSum a (SPFun b c) 
     | SPSum a (SPProd b c) => SPSum a (SPProd b c)
     | SPSum a (SPUnit) => SPSum a (SPUnit) 
     | SPSum a (SPSum b c) => SPSum a (SPSum b c)
   end.

Definition SP_reduceL1 (s:SP TV) : SP TV
:= match s with
     | SPProd SPUnit x => x
     | SPProd (SPConst c) x => SPProd (SPConst c) x
     | SPProd (SPCol m t) x => SPProd (SPCol m t) x
     | SPProd (SPFun a b) x => SPProd (SPFun a b) x
     | SPProd (SPProd y z) x =>  SPProd (SPProd y z) x
     | SPProd (SPSum a b ) x => SPProd (SPSum a b ) x
     | SPProd SPZero x => SPProd SPZero x
     | SPZero => SPZero
     | SPUnit => SPUnit
     | SPConst c => SPConst c
     | SPCol a b => SPCol a b
     | SPFun a b => SPFun a b 
     | SPSum SPZero a => a
     | SPSum (SPConst c) a => SPSum (SPConst c) a 
     | SPSum (SPCol b c) a => SPSum (SPCol b c) a
     | SPSum (SPFun b c) a => SPSum (SPFun b c) a 
     | SPSum (SPProd b c) a => SPSum (SPProd b c) a
     | SPSum (SPUnit) a => SPSum (SPUnit) a
     | SPSum (SPSum b c) a => SPSum (SPSum b c) a
   end.

Fixpoint SP_reducen (n:nat) (s:SP TV) {struct n}: SP TV
  := match n with
       | 0 => s
       | S n' => SP_reduceL1 (SP_reduceR1 ( match s with
                                | SPProd x y => SPProd (SP_reducen n' x) (SP_reducen n' y)
                                | SPZero => SPZero
                                | SPUnit => SPUnit
                                | SPSum x y => SPSum (SP_reducen n' x) (SP_reducen n' y)
                                | SPConst c => SPConst c
                                | SPFun a b => SPFun a (SP_reducen n' b)
                                | SPCol m t => SPCol m (SP_reducen n' t)
                              end))
     end.

Eval compute in (SP_reducen 1000 (evaln 100 (there TV 4 ex_emof_diagram Column))).
Eval compute in (SP_reducen 1000 (there TV 4 ex_emof_diagram Column)).
Eval compute in (SP_reducen 1000 (there TV 4 ex_emof_diagram Named)).
Eval compute in (SP_reducen 1000 (there TV 4 ex_emof_diagram TType)).
Eval compute in (SP_reducen 1000 (there TV 4 ex_emof_diagram Table)).


Definition CG_reduceR1 {s:SP TV} : ClassGraph TV ENV s -> ClassGraph TV ENV (SP_reduceR1 s)
:=  fun x => 
  match x in ClassGraph _ _ s return ClassGraph TV ENV (SP_reduceR1 s)
    with
    | CGProd a SPUnit x y => x
    | CGProd a (SPConst c) x y => CGProd a (SPConst c) x y 
    | CGConst a b => CGConst a b
    | CGCol a b c => CGCol a b c
    | CGFun a b c => CGFun a b c
    | CGProd a (SPCol m b) x y => CGProd a (SPCol m b) x y 
    | CGProd a (SPFun b c) x y => CGProd a (SPFun b c ) x y 
    | CGProd a (SPProd b c) x y => CGProd a (SPProd b c) x y 
    | CGProd a (SPSum b c) x y => CGProd a (SPSum b c) x y
    | CGProd a (SPZero) x y => CGProd a (SPZero) x y
    | CGUnit => CGUnit
    | CGSumLeft a SPZero x => x 
    | CGSumLeft a (SPConst c) x => CGSumLeft a (SPConst c) x
    | CGSumLeft a (SPCol b c) y => CGSumLeft a (SPCol b c) y
    | CGSumLeft a (SPFun b c) y => CGSumLeft a (SPFun b c) y
    | CGSumLeft a (SPProd b c) y => CGSumLeft a (SPProd b c) y
    | CGSumLeft a (SPUnit) x => CGSumLeft a (SPUnit) x
    | CGSumLeft a (SPSum b c) x => CGSumLeft a (SPSum b c) x
(*     | SPSum a (SPProd b c) => SPSum a (SPProd b c)
     | SPSum a (SPUnit) => SPSum a (SPUnit) 
     | SPSum a (SPSum b c) => SPSum a (SPSum b c)*)
    | CGSumRight a (SPConst c) x => CGSumRight a (SPConst c) x
    | CGSumRight a (SPCol b c) x => CGSumRight a (SPCol b c) x
    | CGSumRight a (SPFun b c) x => CGSumRight a (SPFun b c) x
    | CGSumRight a (SPProd b c) x => CGSumRight a (SPProd b c) x
    | CGSumRight a (SPUnit) x => CGSumRight a (SPUnit) x
    | CGSumRight a (SPSum b c) x => CGSumRight a (SPSum b c) x
    | CGSumRight a (SPZero) x => match (CGZero_Inv x) with end 
  end.

Definition CG_reduceL1 {s:SP TV} : ClassGraph TV ENV s -> ClassGraph TV ENV (SP_reduceL1 s)
:=  fun x => 
  match x in ClassGraph _ _ s return ClassGraph TV ENV (SP_reduceL1 s)
    with
    | CGProd SPUnit a _ y => y
    | CGProd (SPConst c) a x y => CGProd (SPConst c) a x y 
    | CGConst a b => CGConst a b
    | CGCol a b c => CGCol a b c
    | CGFun a b c => CGFun a b c
    | CGProd (SPCol m b) a x y => CGProd (SPCol m b) a x y 
    | CGProd (SPFun b c) a x y => CGProd (SPFun b c ) a x y 
    | CGProd (SPProd b c) a x y => CGProd (SPProd b c) a x y 
    | CGProd (SPSum b c) a x y => CGProd (SPSum b c) a x y
    | CGProd (SPZero) a x y => CGProd (SPZero) a x y
    | CGUnit => CGUnit
    | CGSumLeft SPZero a x => match (CGZero_Inv x) with end 
    | CGSumLeft (SPConst c) a x => CGSumLeft (SPConst c) a x
    | CGSumLeft (SPCol b c) a y => CGSumLeft (SPCol b c) a y
    | CGSumLeft (SPFun b c) a y => CGSumLeft (SPFun b c) a y
    | CGSumLeft (SPProd b c) a y => CGSumLeft (SPProd b c) a y
    | CGSumLeft (SPUnit) a x => CGSumLeft (SPUnit) a x
    | CGSumLeft (SPSum b c) a x => CGSumLeft (SPSum b c) a x
(*     | SPSum a (SPProd b c) => SPSum a (SPProd b c)
     | Spsum a (SPUnit) => SPSum a (SPUnit) 
     | SPSum a (SPSum b c) => SPSum a (SPSum b c)*)
    | CGSumRight (SPConst c) a x => CGSumRight (SPConst c) a x
    | CGSumRight (SPCol b c) a x => CGSumRight (SPCol b c) a x
    | CGSumRight (SPFun b c) a x => CGSumRight (SPFun b c) a x
    | CGSumRight (SPProd b c) a x => CGSumRight (SPProd b c) a x
    | CGSumRight (SPUnit) a x => CGSumRight (SPUnit) a x
    | CGSumRight (SPSum b c) a x => CGSumRight (SPSum b c) a x
    | CGSumRight (SPZero) a x => x
  end.


Fixpoint CG_reducen (n:nat) {s:SP TV} {struct n} : ClassGraph TV ENV s -> ClassGraph TV ENV (SP_reducen n s)
:= fun x =>
  match n return ClassGraph TV ENV (SP_reducen n s) with
    | 0 => x
    | S n' => match x in ClassGraph _ _ s return ClassGraph TV ENV (SP_reducen (S n') s)
                with
                | CGProd a b x y => 
                  CG_reduceL1 (CG_reduceR1 (CGProd (SP_reducen n' a) (SP_reducen n' b) (CG_reducen n' x) (CG_reducen n' y)))
                | CGUnit => CG_reduceL1 (CG_reduceR1 (CGUnit))
                | CGSumLeft a b x => 
                  CG_reduceL1 (CG_reduceR1 (CGSumLeft (SP_reducen n' a) (SP_reducen n' b) (CG_reducen n' x)))
                | CGSumRight a b y => 
                  CG_reduceL1 (CG_reduceR1 (CGSumRight (SP_reducen n' a) (SP_reducen n' b) (CG_reducen n' y)))
                | CGConst c i => CGConst c i
                | CGFun t u f => CGFun t (SP_reducen n' u) (fun x => CG_reducen n' (f x))
                | CGCol m t l => 
                  CGCol m (SP_reducen n' t) (LUmap (CG_reducen n') l)
              end
  end.


  
Eval compute in (SP_reducen 10 SP_ttype).
Eval compute in (evaln 100 SP_ttype).
Print ttype_string.
Check (CG_reducen 100 ttype_string').
Eval compute in (CG_reducen 100 ttype_string').
Eval compute in (CG_reducen 100 column_name').

Eval compute in (column_name).
Eval compute in (simplify 100 column_name).
(*Definition column_name' : ClassGraph TV ENV (evaln 100 SP_column).
simpl.
constructor.
constructor.
constructor.
constructor.
constructor.
apply Vcons.
apply CGSumLeft.
exact (simplify 100 ttype_string).
apply Vnil.
constructor.
constructor.
constructor.
constructor.
constructor.
constructor.
apply ("name"%string).
constructor.
constructor.
constructor.
constructor.
constructor.
Defined.
*)

Eval compute in (CG_reducen 100 column_name').
Eval compute in (SP_reducen 100 (evaln 100 SP_column)).

Check ttype_string.
Print CG_ttype.
Eval compute in (CG_reducen 100 ttype_string').

Eval compute in (CG_reducen 1 (column_name')).

Check column_name.
Eval compute in (simplify 100 column_name).
Eval compute in (simplify 100 ttype_string).

Eval compute in (SP_reducen 100 (there TV 4 ex_emof_diagram Column)).
Check (CG_reducen 100 column_name).


(** Now, we're stuck with the rather difficult construction of infinite terms as it is hard to guess the end of (the translation of) one class and the beginning of another **)
(** Let's get polynomial **)
  